#ifndef UTILITIES_HH
# define UTILITIES_HH

#include "cuddObj.hh"
#include <map>
#include <vector>

using namespace std;

// A time difference
double diffclock(clock_t clock1,clock_t clock2);

// Definition of pow for int
int pow(int base, int power);

// Standard procedure to compute reachable states
BDD *compute_reachable_states(BDD* in_st, BDD* Rt, BDDvector *v, BDDvector *pv,
                              Cudd *bddmgr, int &depth);

// Boolean quantification
BDD *Exists(BDDvector *v, BDD *x, Cudd * mgr);

// Computer !K(!formula)
BDD* check_nK(BDD *x, BDD *Ri, BDDvector *v, BDDvector *pv, Cudd * bddmgr,
              BDD *reach);

// The pre-image of X w.r.t. the temporal relation
BDD* preRt(BDD *x, BDD *Rt, BDDvector *v, BDDvector *pv, Cudd * bddmgr);

// Computer EY(formula) (Yesterday, the past X operator)
BDD* check_EY(BDD *x, BDD *Rt, BDDvector *v, BDDvector *pv, Cudd * bddmgr,
              BDD *reach);

// A shortcut for !EY(! ...)
BDD* check_AY(BDD *x, BDD *Rt, BDDvector *v, BDDvector *pv, Cudd * bddmgr,
              BDD *reach);

// Compute equivalence classes for epistemic relation
vector<BDD *> * compute_EC(BDD *Ri, BDDvector *v, BDDvector *pv, Cudd * bddmgr,
                           BDD *reach);

// Translate a state id into the corresponding BDD
BDD* stateid_to_BDD(int stateid, BDDvector* v, Cudd * bddmgr);



// Compute K at depth one (just for testing, see below Kn and KPR)
BDD* K1(BDD *x, BDD *Rt, BDD *Ri, BDDvector *v, BDDvector *pv,
        vector<BDD*> *EC, Cudd *bddmgr, BDD *reach);

// Compute K at depth two (just for testing, see below for general
// expr.)
BDD* K2(BDD *x, BDD *Rt, BDD *Ri, BDDvector *v, BDDvector *pv,
        vector<BDD*> *EC, Cudd *bddmgr, BDD *reach);




// Compute bounded K at depth n
BDD* Kn(int n, BDD *x, BDD *Rt, BDD *Ri, BDDvector *v, BDDvector *pv, 
        vector<BDD*> *EC, Cudd *bddmgr, BDD *reach);
// Compute K with perfect recall
BDD* KPR(BDD *x, BDD *Rt, BDD *Ri, BDDvector *v, BDDvector *pv, 
	 vector<BDD*> *EC, Cudd *bddmgr, BDD *reach, int depth);

// Build a test model
void build_test_model(Cudd *bddmgr, BDDvector *v, BDDvector *pv, 
		      BDD *Rt, BDD *Ri, map<string, BDD*> *evaluation);

// Build a "deep" model (to test)
void build_deep_model(int n, Cudd *bddmgr, BDDvector *v, BDDvector *pv, 
		      BDD *Rt, BDD *Ri, 
		      map<string, BDD*> *evaluation);

// Build a "wide" model (to test)
void build_wide_model(int w, int d, Cudd *bddmgr, BDDvector *v, BDDvector *pv, 
		      BDD *Rt, BDD *Ri, 
		      map<string, BDD*> *evaluation);
#endif // ! UTILITIES_HH




